Nuprl Lemma : rel_exp_functionality_wrt_brle
11,40
postcript
pdf
n
:
,
T
:Type,
R1
,
R2
:(
T
T
). (
R1
>{
T
}
R2
)
(rel_exp(
T
;
R1
;
n
)
>{
T
} rel_exp(
T
;
R2
;
n
))
latex
Definitions
R1
=>
R2
,
x
f
y
Lemmas
rel
exp
functionality
wrt
rel
implies
origin
n:
, T:Type, R1, R2:(T
T
). (R1 
>{T} R2) 
(rel_exp(T;R1;n) >{T} rel_exp(T;R2;n)) n:, T:Type, R1, R2:(TT). (R1 >{T} R2) (rel_exp(T;R1;n) >{T} rel_exp(T;R2;n))